membert(X,(X)) :- atom(X).
membert(X,(X,_)).
membert(X,(_,Y)) :- membert(X,Y).

conlist([],""):-!.
conlist([Str],Str):-!.
conlist([Str1,Str2],Res):-
	concat(Str1,Str2,Res),!.
conlist([H|T],Res):-
	conlist(T,Temp),
	concat(H,Temp,Res).

sep(_,[],N,N). sep(_,[S],_,S) :- !. sep(SEP,[X|LST],N,STR) :- sep(SEP,LST,N,SLST), conlist([X,SEP,SLST],STR).

sep(A,B,C) :- sep(A,B,'',C).

% ----- symbolic message to string ----------------------------------------------------------------------------------------------------------------------------------

% e.g. S1='pi_'
stringrepr('\\_', X) :- not(ground(X)), !. 
stringrepr(S, (A,2)) :- stringrepr(S1,A), conlist(['{',S1,'}\''],S), !.
stringrepr(S, (A,B)) :- stringrepr(S1,A), stringrepr(S2,B), conlist([S1,',',S2],S), !.
stringrepr(S, ss((A,B),C)) :- stringrepr(S1,A),stringrepr(S2,B),stringrepr(S3,C),conlist([S3,'[',S1,'_{',S2,'}]'],S), !.
stringrepr(S, ss(A,B)) :- stringrepr(S1,A),stringrepr(S2,B),conlist([S2,'[',S1,']'],S), !.
stringrepr('\\cdot', dot) :- !.
stringrepr(S, X) :- string_to_atom(S1, X), stringrepr2(S1, S).

% e.g. S1='pi_1_', S='\pi_{1}'
stringrepr2(S1, S) :- concat(S2,'_',S1), stringrepr2(S2,S3), concat('\\',S3,S), !.
stringrepr2(S1, S) :- concat(S2, S3, S1), concat('_', S4, S3), stringrepr3(S2,S22), stringrepr3(S4, S44), string_length(S4, L), L>1, conlist([S22,'_{',S44,'}'], S), !.
stringrepr2(S1, S) :- concat(S2, S3, S1), concat('_', S4, S3), stringrepr3(S2,S22), stringrepr3(S4, S44), string_length(S4, 1),      conlist([S22,'_{',S44,'}'], S), !.
stringrepr2(S1,S) :- stringrepr3(S1,S).

% e.g. S1='a_b', S='a,b'
% the following is hugely inelegant and inefficient, but hey, it seems to work..
stringrepr3(S1, S) :- concat(S2, S3, S1), concat('_', S4, S3), stringrepr3(S2, S22), stringrepr3(S4, S44), conlist([S22,',',S44], S), !.
stringrepr3(S1, S) :- concat(S2, S3, S1), concat('I', S4, S3), stringrepr3(S2, S22), stringrepr3(S4, S44), conlist([S22,'\'',S44], S), !.
stringrepr3(S1, S) :- concat(S2, S3, S1), concat('P', S4, S3), stringrepr3(S2, S22), stringrepr3(S4, S44), conlist([S22,'^+',S44], S), !.
stringrepr3(S1, S) :- concat(S2, S3, S1), concat('M', S4, S3), stringrepr3(S2, S22), stringrepr3(S4, S44), conlist([S22,'^-',S44], S), !.
stringrepr3(S,S).

list_commastr([],'') :- !.
list_commastr([S],S) :- !.
list_commastr([S1|L], S) :-
  list_commastr(L,S2),
  conlist([S1, ', ', S2], S).

string_to('\\cdot',dot) :- !.
string_to(S,LST) :- list_commastr(LST,S).

string_from(';\\bot', bot) :- !.
string_from('', dot) :- !.
string_from(';\\cdot', []) :- !.
string_from(ST,LST) :- list_commastr(LST,S), conlist([';',S],ST).

string_message0(S, M) :- M=mp(A,B), string_message(SA,A), string_message(SB,B), conlist([SA,'{\\doteq}',SB],S).
string_message0('\\{\\}', []) :- !.
string_message0(S,N) :- number(N), stringrepr(SN,N), conlist(['\\mathsf{m}_{', SN, '}'], S).

string_message0(S, X) :- atom(X), stringrepr(S,X).

string_message0(S,M) :- M=cm((V,F),TO,FROM), !, string_message(SOR,cm(V,TO,FROM)), stringrepr(SF,F), conlist(['\\symsumat{', SOR, '}{', SF, '}{?}'], S).
string_message0(S,M) :- M=cmr((V,F),TO,FROM), !, string_message(SOR,cmr(V,TO,FROM)), stringrepr(SF,F), conlist(['\\symsumat{', SOR, '}{', SF, '}{?}'], S).

%%%cmr(V,dot,bot) \def\instdatar#1#2{\ctxm{\mathbf{#1}}{#2}{\cdot;\bot}}  
%%string_message0(S,M) :- M=cmr(V,dot,bot), !,  stringrepr(SV,V), conlist(['\\instdatar{', SV, '}{}'], S).
%%%cmr(V,dot,dot) \def\ninstdatar#1#2{\ctxm{\mathbf{#1}}{#2}{\cdot}}      
%%string_message0(S,M) :- M=cmr(V,dot,dot), !,  stringrepr(SV,V), conlist(['\\ninstdatar{', SV, '}{}'], S).
%%%cm(V,dot,dot)  \def\ninstdata#1#2{\ctxm{#1}{#2}{\cdot}}                
%%string_message0(S,M) :- M=cm(V,dot,dot), !,  stringrepr(SV,V), conlist(['\\ninstdata{', SV, '}{}'], S).
%%%cmr(V,LST,bot) \def\sessionidr#1#2#3{\ctxm{\mathbf{#1}}{#2}{#3;\bot}}  
%%string_message0(S,M) :- M=cmr(V,TO,bot), !,  stringrepr(SV,V), list_commastr(TO,TOS), conlist(['\\sessionidr{', SV, '}{}{', TOS, '}'], S).
%%%cm(V,LST,bot) \def\sessionid#1#2#3{\ctxm{#1}{#2}{#3;\bot}}            
%%string_message0(S,M) :- M=cm(V,TO,bot), !,  stringrepr(SV,V), list_commastr(TO,TOS), conlist(['\\sessionidr{', SV, '}{}{', TOS, '}'], S).
%%%cm(V,LST,dot) \def\di#1#2#3{\ctxm{#1}{#2}{#3}}                        
%%string_message0(S,M) :- M=cm(V,TO,dot), !,  stringrepr(SV,V), list_commastr(TO,TOS), conlist(['\\di{', SV, '}{}{', TOS, '}'], S).
%%%cmr(V,LST,[]) \def\globalidr#1#2#3{\ctxm{\mathbf{#1}}{#2}{#3;\cdot}}  
%%string_message0(S,M) :- M=cmr(V,TO,[]), !,  stringrepr(SV,V), list_commastr(TO,TOS), conlist(['\\globalidr{', SV, '}{}{', TOS, '}'], S).
%%%cm(V,LST,[])  \def\globalid#1#2#3{\ctxm{#1}{#2}{#3;\cdot}}            
%%string_message0(S,M) :- M=cm(V,TO,[]), !,  stringrepr(SV,V), list_commastr(TO,TOS), conlist(['\\globalid{', SV, '}{}{', TOS, '}'], S).
%%%cm(V,LST,LST) \def\id#1#2#3#4{\ctxm{#1}{#2}{#3;#4}}                   
%%string_message0(S,M) :- M=cm(V,TO,FROM), !,  stringrepr(SV,V), list_commastr(TO,TOS), list_commastr(FROM,FROMS), conlist(['\\id{', SV, '}{}{', TOS, '}{', FROMS, '}'], S).

%% (without multiple data subjects extension)
%string_message0(S,M) :- M=cmr(V,dot,bot), !,  stringrepr(SV,V), conlist(['\\ctxm{\\instrandom{', SV, '}}{}{\\cdot}'], S).
%string_message0(S,M) :- M=cmr(V,dot,dot), !,  stringrepr(SV,V), conlist(['\\ctxm{\\mathbf{', SV, '}}{}{\cdot}'], S).
%string_message0(S,M) :- M=cm(V,dot,dot), !,  stringrepr(SV,V), conlist(['\\ctxm{', SV, '}{}{\cdot}'], S).
%string_message0(S,M) :- M=cm(V,[TO],dot), !,  stringrepr(SV,V), stringrepr(TOS,TO), conlist(['\\ctxm{', SV, '}{}{', TOS, '}'], S).
%string_message0(S,M) :- M=cmr(V,[TO],[]), !,  stringrepr(SV,V), stringrepr(TOS,TO), conlist(['\\ctxm{\\mathbf{', SV, '}}{}{', TOS, '}'], S).
%string_message0(S,M) :- M=cm(V,[TO],[]), !,  stringrepr(SV,V), stringrepr(TOS,TO), conlist(['\\ctxm{', SV, '}{}{', TOS, '}'], S).

%(with multiple data subjects extension)
  %Data item           &  D/k                       & $\ctxm{d}{\kappa}{p_1,\ldots,p_k;\top}$      & $d|_1,\ldots,d|_k$ \\
  %Global identifier   & I/k                        & $\ctxm{i}{\kappa}{p_1,\ldots,p_k;\emptyset}$ & $i|_1,\ldots,i|_k$ \\
  %Local identifier    & I/k/l                      & $\ctxm{i}{\kappa}{p_1,\ldots,p_k;q_1,\ldots,q_l}$ & $i|_1,\ldots,i|_k,i|_{;1},\ldots,i|_{;l}$ \\
string_message0(S,M) :- M=cmr(V,dot,bot), !,  stringrepr(SV,V),                                                  conlist(['\\ctxm{\\instrandom{', SV, '}}{}{\\cdot}'], S).
string_message0(S,M) :- M=cmr(V,dot,dot), !,  stringrepr(SV,V),                                                  conlist(['\\ctxm{\\mathbf{', SV, '}}{}{\\cdot}'], S).
string_message0(S,M) :- M=cm(V,dot,dot), !,  stringrepr(SV,V),                                                   conlist(['\\ctxm{', SV, '}{}{\\cdot}'], S).
string_message0(S,M) :- M=cmr(V,TO,bot), !,  stringrepr(SV,V), list_commastr(TO,TOS),                            conlist(['\\ctxm{\\instrandom{', SV, '}}{}{', TOS, '}'], S).
string_message0(S,M) :- M=cm(V,TO,bot), !,  stringrepr(SV,V), list_commastr(TO,TOS),                             conlist(['\\ctxm{', SV, '}{}{', TOS, ';\\top}'], S).
string_message0(S,M) :- M=cm(V,TO,dot), !,  stringrepr(SV,V), list_commastr(TO,TOS),                             conlist(['\\ctxm{', SV, '}{}{', TOS, ';\\top}'], S).
string_message0(S,M) :- M=cmr(V,TO,[]), !,  stringrepr(SV,V), list_commastr(TO,TOS),                             conlist(['\\ctxm{\\mathbf{', SV, '}}{}{', TOS, ';\\emptyset}'], S).
string_message0(S,M) :- M=cm(V,TO,[]), !,  stringrepr(SV,V), list_commastr(TO,TOS),                              conlist(['\\ctxm{', SV, '}{}{', TOS, ';\\emptyset}'], S). 
string_message0(S,M) :- M=cm(V,TO,FROM), !,  stringrepr(SV,V), list_commastr(TO,TOS), list_commastr(FROM,FROMS), conlist(['\\ctxm{', SV, '}{}{', TOS, ';', FROMS,'}'], S). 


% ----- messages --------------------------------------------------------------

% old notation for signature with plaintext recovery
string_message0(S,pri(lst,[M2,pri(s,[M1,M2])])) :- !, string_message(S,pri(sigr,[M2,M1])).

string_message0(S, pri(lst,L)) :-
  findall(X,(member(I,L),string_message(X,I)),L2),
  list_commastr(L2,S1),
  conlist(['\\{',S1,'\\}'], S), !.
  
string_message0(S, L) :- is_list(L), findall(X,(member(I,L),string_message(X,I)),L2), list_commastr(L2,S).

% compatibility mode for old primitive names
string_message0(S,pri(hash,M)) :- !, string_message(S,pri(h,M)).
string_message0(S,pri(es,[K,M])) :- !, string_message(S,pri(enc,[M,K])).
string_message0(S,pri(ea,[K,M])) :- !, string_message(S,pri(aenc,[M,K])).
string_message0(S,pri(el,[K,M,L])) :- !, string_message(S,pri(aencl,[M,L,K])).
string_message0(S,pri(s,[K,M])) :- !, string_message(S,pri(sig,[M,K])).
string_message0('\\emptyset',pri(naught,[])) :- !.

string_message0(S, pri((sum,F),[M])) :-
  string_message(S1,M),
  string_message(SF,F),
  conlist(['\\symsum{',S1,'}{',SF,'}'], S).

% standard messages
string_message0(S, pri(T,L)) :-
  findall(X,(member(I,L),string_message(X,I)),L2),
  list_commastr(L2,S1),
  conlist(['\\mathsf{', T, '}(', S1, ')'], S).
  
  
string_message(S,M) :- string_message0(S,M), !.
string_message(_,M) :- print('*** string_message failed: M='), print(M), print('\n').

% string from disjunction of constraints
string_constraintd('\\top',[]).
string_constraintd(SM,[M]) :- !, string_message(SM,M).
string_constraintd(SRET,[X|LST]) :- string_message(SX,X), string_constraintd(SLST,LST), conlist([SX,' \\wedge ', SLST], SRET).

% string from conjunction of disjunction of constraints
string_constraints('\\top',[]).
string_constraints(MS,[M]) :- !, string_constraintd(MS,M).
string_constraints(MS,[X|LST]) :- string_constraintd(SX,X), string_constraints(SLST,LST), conlist([SX,'\\vee ',SLST], MS).

% ---- print tables and entries


printtable(PR,R,KBN) :-
  forall((member((M,REQ),KBN),M\=pri(lst,_),M\=pri((sum,_),_),not(local(M))),(print('dertable('), print(PR), print(','), print(R), print(','), print(M), print(','), print(REQ), print(').\n'))).

printinternalce(KBN) :-
  print('% possible internal CEs\n'),
  forall((member((M,_),KBN),member((MP,_),KBN),M\=cm(_,_,_),MP\=cm(_,_,_),M\=cmr(_,_,_),MP\=cmr(_,_,_),M\=pri(lst,_),MP\=pri(lst,_),M\=pri((sum,_),_),MP\=pri((sum,_),_),M\=MP,cecint(M,MP,_)),(print('% ** '),print(M),print(' ?=? '),print(MP),print('\n'))),
  print('% end\n').

printmessage(M) :-
  string_message(MS,M),print('$'),print(MS),print('$\n\n').



string_other(RET,(PR,ROLE,M,[])) :- !,
  string_to_atom(SPR,PR),string_to_atom(SROLE,ROLE),
  string_message(SM,M),
  conlist([SPR,':',SROLE, ': $',SM,'$'],RET).
string_other(RET,(PR,ROLE,M,ACTS)) :-
  string_to_atom(SPR,PR),string_to_atom(SROLE,ROLE),
  string_message(SM,M),
  findall(SACT, (member((ACTL,ACTR),ACTS),conlist(['$\\ecos{',ACTL,'}{',ACTR,'}$'],SACT)),SACTS), sep(',',SACTS,SACTS1),
  conlist([SPR,':',SROLE, ': $',SM,'$ (', SACTS1, ')'], RET).

string_others(RET,LST) :-
  findall((PR2,R2,CONSTR2),member((PR2,R2,_,CONSTR2),LST),PRCLIST), list_to_set(PRCLIST,PRCSET),
  findall(SRET,(member((PR2,R2,CONSTR2),PRCSET),
                findall(M,member((PR2,R2,M,CONSTR2),LST),ML),
                string_other(SRET,(PR2,R2,ML,CONSTR2))),SRETS),
  sep(';\\\\&',SRETS,RET).

printentryreqs(M,REQS) :-
  print('$'),
  string_constraints(REQSS,REQS),print(REQSS),
  print(' {\\Rightarrow} '),
  string_message(MS,M),print(MS),
  print('$\\\\\n').

printentryce(M) :-
  string_message(MS,M),print('$'),print(MS),print('$&'),
  findall((PR2,R2,M2,CONSTR2S),(dertable(PR2,R2,M2,REQ2),cecact(M,M2,CONSTR2),list_to_set(CONSTR2,CONSTR2S),member(REQL,REQ2),not(member(M2,REQL))),LSTOTHER),
  list_to_set(LSTOTHER,SETOTHER),
  string_others(STRINGOTHER,SETOTHER),print(STRINGOTHER),
  print('\\\\\\hline\n').

printinternalcetex(KBN) :-
    forall((member((M,_),KBN),member((MP,_),KBN),M\=cm(_,_,_),MP\=cm(_,_,_),M\=cmr(_,_,_),MP\=cmr(_,_,_),M\=pri(lst,_),MP\=pri(lst,_),M\=pri((sum,_),_),MP\=pri((sum,_),_),M\=MP,cecint(M,MP,_)),(
      string_message(MS,M),
      string_message(MPS,MP),
      print('$'),print(MS),print(' ?=? '),print(MPS),print('$\n\n')
    )).


printentrylinks(PR,M) :- not((dertable(_,_,M2,_),ceclink(PR,M,M2,_))), !.

printentrylinks(PR,M) :-
  string_message(MS,M),print('$'),print(MS),print('$&'),
  findall((PR2,R2,M2,CONSTR2S),(dertable(PR2,R2,M2,_),ceclink(PR,M,M2,CONSTR2),list_to_set(CONSTR2,CONSTR2S)),LSTOTHER),
  list_to_set(LSTOTHER,SETOTHER),
  string_others(STRINGOTHER,SETOTHER),print(STRINGOTHER),
  print('\\\\\\hline\n').



freeit(X,X) :- var(X), !.
freeit([X|_],V) :- freeit(X,V), !.
freeit([_|LST],V) :- freeit(LST,V), !.
freeit(pri(_,LST),V) :- freeit(LST,V), !.

replaceit(V1,V2,V1P,V2) :- V1==V1P, !.
replaceit(V1,V2,LST,[X2|LST2]) :- is_list(LST), LST=[X1|LST1], replaceit(V1,V2,X1,X2), replaceit(V1,V2,LST1,LST2), !.
replaceit(V1,V2,pri(X,L1),pri(X,L2)) :- ground(X), replaceit(V1,V2,L1,L2), !.
replaceit(_,_,X,X).

% TODO: generalise to any number of messages
mkgr([CM|CMP],M1,M2) :- freeit(M1,Z), !, replaceit(Z,CM,M1,M1P), mkgr(CMP,M1P,M2).
mkgr(_,M1,M1).
mkgr(M1,M2) :- mkgr([1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25],M1,M2).


containsm(X,X).
containsm(M,Y) :- M=pri(T,_), ground(T), consneeded(M,LST), member(X,LST), containsm(X,Y).
containsm(pri((sum,FAM),M1),M3) :- ground(FAM), putfam(FAM,M1,M2), containsm(M2,M3).
containsm(L,Y) :- is_list(L), member(I,L), containsm(I,Y).

findprims(SET) :- findall((T,L),(protoknow(_,_,Y),containsm(Y,X),X=pri(T,LST),T\=(sum,_),T\=lst,length(LST,L)),LST),list_to_set(LST,SET).

genvar(_).
genvars(0,[]) :- !.
genvars(NP1,[_|LST]) :- N is NP1-1, genvars(N,LST).

printprim((T,L)) :-
  print('\\textbf{Primitive '), print(T), print('}\n\n'),
  forall((genvars(L,LST),
         consneeded(pri(T,LST),X),
         mkgr([LST,X],[LSTG,XG]),
         string_message(SM,pri(T,LSTG)),
         string_message(SLST,XG),
         conlist(['$\\construct{', SM, '}{', SLST,'}'],STR)),(print(STR),print('$\n\n'))),
  forall((genvars(L,LST),
         elneeded(pri(T,LST),X,REQ),
         mkgr([LST,X,REQ],[LSTG,XG,REQG]),
         string_message(SM,pri(T,LSTG)),
         string_message(SX,XG),
         string_message(SREQ,REQG),
         conlist(['$\\eliminate{', SM, '}{', SREQ,'}{', SX, '}'],STR)),(print(STR),print('$\n\n'))),
  print('\n\n').

printprims :- findprims(SET),forall(member(X,SET),printprim(X)).

